Nuprl Lemma : qoset_lt_irrefl 13,42

s:QOSet, a, b:|s|. (a <s b)  ((a = b)) 
latex


Upsets 1
Definitions of StatementDSet, QOSet
Definitionst  T, P  Q, x:A. B(x), x,y. t(x;y), DSet, QOSet, x(s1,s2), P & Q, P  Q,
Lemmasqoset wf, set car wf, set lt wf, set leq wf, strict part irrefl, set lt is sp of leq

origin